Calculus of Constructions
- 타입 이론
Calculus of Constructions (CoC)는 타입 이론의 한가지이다. Coq 등의 증명보조기의 기반이론으로 이용된다. Impredicative \(\mathrm{Prop}\) 유니버스를 가지고 있다는 점에서 마틴뢰프 타입 이론과 구분된다.
Calculus of Inductive Constructions (CIC)
귀납적 타입을 추가한 CoC의 변종이다.
Calculus of Constructions (CoC)는 타입 이론의 한가지이다. Coq 등의 증명보조기의 기반이론으로 이용된다. Impredicative \(\mathrm{Prop}\) 유니버스를 가지고 있다는 점에서 마틴뢰프 타입 이론과 구분된다.
귀납적 타입을 추가한 CoC의 변종이다.